Module isotope::term [−][src]
Expand description
Terms in isotope
’s underlying dependent type system
Modules
dynamic | Dynamic terms, which allow run-time extension of |
flags | Flags for |
weak | Weak references to |
Structs
Annotation | An owned type annotation |
App | A function application, with an optional type annotation |
Case | A case expression, which switches on variants to return a value |
Code | The hash-code of a value |
Enum | A type with a finite number of named variants |
Id | The identity type, representing proofs that two terms are equal |
Lambda | A lambda function |
Pi | A dependent function type |
Refl | The reflexivity axiom: asserts that the left hand side and right hand side are judgementally equal, and therefore propositionally equal |
TermId | A term in |
Universe | A typing universe |
UniverseTerm | A term containing a typing universe |
Var | A variable, represented by a de-Bruijn index |
VarFilter | A filter for variables |
Variant | A variant of an enumeration |
Enums
AnnotationRef | A borrowed type annotation |
Form | Forms a term can be in |
Term | An enumeration of terms in |
Traits
AnnotationLike | A term which behaves like a (potentially borrowed) annotation |
Cons | Objects which can be consed in a context |
HasDependencies | Objects which have value dependencies |
OptionalValue | A convenience trait implemented by |
Substitute | Objects which can be substituted in a context |
TermEq | Objects which may be determined equivalent by terms |
Typecheck | Objects which can be type-checked in a context |
Value | A trait implemented by values in |